|
| 1: |
|
minus(x,0) |
→ x |
| 2: |
|
minus(s(x),s(y)) |
→ minus(x,y) |
| 3: |
|
quot(0,s(y)) |
→ 0 |
| 4: |
|
quot(s(x),s(y)) |
→ s(quot(minus(x,y),s(y))) |
| 5: |
|
le(0,y) |
→ true |
| 6: |
|
le(s(x),0) |
→ false |
| 7: |
|
le(s(x),s(y)) |
→ le(x,y) |
| 8: |
|
app(nil,y) |
→ y |
| 9: |
|
app(add(n,x),y) |
→ add(n,app(x,y)) |
| 10: |
|
low(n,nil) |
→ nil |
| 11: |
|
low(n,add(m,x)) |
→ if_low(le(m,n),n,add(m,x)) |
| 12: |
|
if_low(true,n,add(m,x)) |
→ add(m,low(n,x)) |
| 13: |
|
if_low(false,n,add(m,x)) |
→ low(n,x) |
| 14: |
|
high(n,nil) |
→ nil |
| 15: |
|
high(n,add(m,x)) |
→ if_high(le(m,n),n,add(m,x)) |
| 16: |
|
if_high(true,n,add(m,x)) |
→ high(n,x) |
| 17: |
|
if_high(false,n,add(m,x)) |
→ add(m,high(n,x)) |
| 18: |
|
quicksort(nil) |
→ nil |
| 19: |
|
quicksort(add(n,x)) |
→ app(quicksort(low(n,x)),add(n,quicksort(high(n,x)))) |
|
There are 18 dependency pairs:
|
| 20: |
|
MINUS(s(x),s(y)) |
→ MINUS(x,y) |
| 21: |
|
QUOT(s(x),s(y)) |
→ QUOT(minus(x,y),s(y)) |
| 22: |
|
QUOT(s(x),s(y)) |
→ MINUS(x,y) |
| 23: |
|
LE(s(x),s(y)) |
→ LE(x,y) |
| 24: |
|
APP(add(n,x),y) |
→ APP(x,y) |
| 25: |
|
LOW(n,add(m,x)) |
→ IF_LOW(le(m,n),n,add(m,x)) |
| 26: |
|
LOW(n,add(m,x)) |
→ LE(m,n) |
| 27: |
|
IF_LOW(true,n,add(m,x)) |
→ LOW(n,x) |
| 28: |
|
IF_LOW(false,n,add(m,x)) |
→ LOW(n,x) |
| 29: |
|
HIGH(n,add(m,x)) |
→ IF_HIGH(le(m,n),n,add(m,x)) |
| 30: |
|
HIGH(n,add(m,x)) |
→ LE(m,n) |
| 31: |
|
IF_HIGH(true,n,add(m,x)) |
→ HIGH(n,x) |
| 32: |
|
IF_HIGH(false,n,add(m,x)) |
→ HIGH(n,x) |
| 33: |
|
QUICKSORT(add(n,x)) |
→ APP(quicksort(low(n,x)),add(n,quicksort(high(n,x)))) |
| 34: |
|
QUICKSORT(add(n,x)) |
→ QUICKSORT(low(n,x)) |
| 35: |
|
QUICKSORT(add(n,x)) |
→ LOW(n,x) |
| 36: |
|
QUICKSORT(add(n,x)) |
→ QUICKSORT(high(n,x)) |
| 37: |
|
QUICKSORT(add(n,x)) |
→ HIGH(n,x) |
|
The approximated dependency graph contains 7 SCCs:
{24},
{23},
{29,31,32},
{25,27,28},
{20},
{34,36}
and {21}.